E-State{i:l}  Type{i'} 

latex

Definitions	suptype(S; T), S  T, P  Q, x,y. t(x;y), x. t(x), x:A. B(x), Top, EventsWithState, t  T, P & Q, x(s1,s2), x(s), , EOrderAxioms(E; pred?; info)
Lemmas	top wf, first wf, assert wf, not wf, val-axiom wf, rationals wf, nat wf, Msg wf, loc wf, kind wf, kindcase wf, Knd wf, EState wf, EOrderAxioms wf, IdLnk wf, Id wf, unit wf, deq wf